(declare-fun _substvar_18_ () Real)
(declare-const r3 Real)
(declare-const r5 Real)
(declare-const r6 Real)
(declare-const r8 Real)
(declare-const r9 Real)
(declare-const r13 Real)
(declare-const r19 Real)
(declare-const r22 Real)
(assert (>= (/ (- 0.399331 r3 r19 r13) r19) 33.0 r19 _substvar_18_))
(check-sat)
